(set-logic QF_NRA)
(declare-fun _substvar_1613_ () Real)
(declare-fun _substvar_1804_ () Real)
(declare-fun _substvar_1823_ () Real)
(declare-fun _substvar_1847_ () Real)
(declare-fun _substvar_1996_ () Real)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r7 Real)
(assert (or (< 0.47 82420.0 _substvar_1804_ r1) (<= 6472545.0 (* r2 6472545.0 (/ (* 82420.0 r1 (+ 6472545.0 82420.0 6472545.0 6472545.0 r1)) r2)) 6472545.0 (- r7) _substvar_1823_)))
(assert (or (< r1 r2 _substvar_1847_ 0.0) (< r1 r2 (/ (+ 6472545.0 82420.0 6472545.0 6472545.0 r1) (* r2 6472545.0 (/ (* 82420.0 r1 (+ 6472545.0 82420.0 6472545.0 6472545.0 r1)) r2))) 0.0)))
(assert (<= 6472545.0 _substvar_1613_ 6472545.0 (- r7) _substvar_1996_))
(check-sat)